Inference at * 2 
Iof proof for Lemma assert of eq int:



1. x : 
2. y : 
3. x = y
  (x = y) 

latex

 by Unfold `eq_int` 0 

latex

 1: 

 1:   if x=y  then tt  else ff
 .

Definitions

(i = j)